$\forall$$A$, $B$:Type, $f$:($A$$\rightarrow$$B$). (Id\{$B$\} o $f$) = $f$